
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Backend.Model.DateTimeModelPart</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Backend.Model.DateTimeModelPart" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Backend.Model.DateTimeModelPart</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.ZArith.ZArith.html">ZArith</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Classes.EquivDec.html">EquivDec</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Classes.Equivalence.html">Equivalence</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Utils.html">Qcert.Utils.Utils</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.ForeignData.html">Qcert.Common.DataModel.ForeignData</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.ForeignOperators.html">Qcert.Common.Operators.ForeignOperators</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.JavaScriptAstRuntime.html">Qcert.JavaScriptAst.JavaScriptAstRuntime</a></span>.<br/>
<br/>
<span class="kwd">Import</span> <span class="id">ListNotations</span>.<br/>
<br/>
<div class="doc">Defines the foreign support for DateTime
     Posits axioms for the basic data/operators, and 
     defines how they are extracted to ocaml (using helper functions
     defined in qcert/ocaml/...../Util.ml)
     </div>
<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_DURATION">DATE_TIME_DURATION</a></span> : <span class="kwd">Set</span>.<br/>
<span class="id">Extract</span> <span class="id">Constant</span> <span class="id">DATE_TIME_DURATION</span> =&gt; "<span class="id">DateTime.duration</span>".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_DURATION_eq">DATE_TIME_DURATION_eq</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_DURATION_eq</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.deq</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="id">Conjecture</span> <span class="id"><a name="DATE_TIME_DURATION_eq_correct">DATE_TIME_DURATION_eq_correct</a></span> :<br/>
&nbsp;&nbsp;<span class="kwd">forall</span> <span class="id">f1</span> <span class="id">f2</span>, (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION_eq">DATE_TIME_DURATION_eq</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f1">f1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f2">f2</a></span> = <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span> &lt;-&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f1">f1</a></span> = <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f2">f2</a></span>).<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_DURATION_to_string">DATE_TIME_DURATION_to_string</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_DURATION_to_string</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">Util.char_list_of_string</span> (<span class="id">DateTime.dto_string</span> <span class="id">x</span>))".<br/>
<br/>
<span class="kwd">Program</span> <span class="kwd">Instance</span> <span class="id"><a name="date_time_duration_foreign_data">date_time_duration_foreign_data</a></span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.ForeignData.html#foreign_data">foreign_data</a></span><br/>
&nbsp;&nbsp;:= {<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.ForeignData.html#foreign_data_type">foreign_data_type</a></span> := <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span>}.<br/>
<div class="toggleproof" onclick="toggleDisplay('proof1')">Next Obligation.</div>
<div class="proofscript" id="proof1">
&nbsp;&nbsp;<span class="tactic">intros</span> <span class="id">x</span> <span class="id">y</span>.<br/>
&nbsp;&nbsp;<span class="id">case_eq</span> (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION_eq">DATE_TIME_DURATION_eq</a></span> <span class="id">x</span> <span class="id">y</span>); <span class="tactic">intros</span> <span class="id">eqq</span>.<br/>
&nbsp;&nbsp;+ <span class="id">left</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">f_equal</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">apply</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION_eq_correct">DATE_TIME_DURATION_eq_correct</a></span> <span class="kwd">in</span> <span class="id">eqq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">trivial</span>.<br/>
&nbsp;&nbsp;+ <span class="id">right</span>; <span class="tactic">intros</span> <span class="id">eqq2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">red</span> <span class="kwd">in</span> <span class="id">eqq2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">apply</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION_eq_correct">DATE_TIME_DURATION_eq_correct</a></span> <span class="kwd">in</span> <span class="id">eqq2</span>. <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">congruence</span>.<br/>
Defined.</div>
<div class="toggleproof" onclick="toggleDisplay('proof2')">Next Obligation.</div>
<div class="proofscript" id="proof2">
&nbsp;&nbsp;<span class="tactic">exact</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Logic.html#True">True</a></span>.<br/>
Defined.</div>
<div class="toggleproof" onclick="toggleDisplay('proof3')">Next Obligation.</div>
<div class="proofscript" id="proof3">
&nbsp;&nbsp;<span class="tactic">reflexivity</span>.<br/>
Qed.</div>
<div class="toggleproof" onclick="toggleDisplay('proof4')">Next Obligation.</div>
<div class="proofscript" id="proof4">
&nbsp;&nbsp;<span class="id">constructor</span>.<br/>
&nbsp;&nbsp;<span class="tactic">intros</span> <span class="id">f</span>.<br/>
&nbsp;&nbsp;<span class="tactic">exact</span> (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION_to_string">DATE_TIME_DURATION_to_string</a></span> <span class="id">f</span>).<br/>
Defined.</div>
<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME">DATE_TIME</a></span> : <span class="kwd">Set</span>.<br/>
<span class="id">Extract</span> <span class="id">Constant</span> <span class="id">DATE_TIME</span> =&gt; "<span class="id">DateTime.dateTime</span>".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_now">DATE_TIME_now</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_now</span> =&gt; "(<span class="id">DateTime.now</span> ())".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_eq">DATE_TIME_eq</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_eq</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.eq</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="id">Conjecture</span> <span class="id"><a name="DATE_TIME_eq_correct">DATE_TIME_eq_correct</a></span> :<br/>
&nbsp;&nbsp;<span class="kwd">forall</span> <span class="id">f1</span> <span class="id">f2</span>, (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_eq">DATE_TIME_eq</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f1">f1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f2">f2</a></span> = <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span> &lt;-&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f1">f1</a></span> = <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f2">f2</a></span>).<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_to_string">DATE_TIME_to_string</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_to_string</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">Util.char_list_of_string</span> (<span class="id">DateTime.to_string</span> <span class="id">x</span>))".<br/>
<br/>
<span class="kwd">Program</span> <span class="kwd">Instance</span> <span class="id"><a name="date_time_foreign_data">date_time_foreign_data</a></span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.ForeignData.html#foreign_data">foreign_data</a></span><br/>
&nbsp;&nbsp;:= {<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.ForeignData.html#foreign_data_type">foreign_data_type</a></span> := <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span>}.<br/>
<div class="toggleproof" onclick="toggleDisplay('proof5')">Next Obligation.</div>
<div class="proofscript" id="proof5">
&nbsp;&nbsp;<span class="tactic">intros</span> <span class="id">x</span> <span class="id">y</span>.<br/>
&nbsp;&nbsp;<span class="id">case_eq</span> (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_eq">DATE_TIME_eq</a></span> <span class="id">x</span> <span class="id">y</span>); <span class="tactic">intros</span> <span class="id">eqq</span>.<br/>
&nbsp;&nbsp;+ <span class="id">left</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">f_equal</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">apply</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_eq_correct">DATE_TIME_eq_correct</a></span> <span class="kwd">in</span> <span class="id">eqq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">trivial</span>.<br/>
&nbsp;&nbsp;+ <span class="id">right</span>; <span class="tactic">intros</span> <span class="id">eqq2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">red</span> <span class="kwd">in</span> <span class="id">eqq2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">apply</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_eq_correct">DATE_TIME_eq_correct</a></span> <span class="kwd">in</span> <span class="id">eqq2</span>. <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="tactic">congruence</span>.<br/>
Defined.</div>
<div class="toggleproof" onclick="toggleDisplay('proof6')">Next Obligation.</div>
<div class="proofscript" id="proof6">
&nbsp;&nbsp;<span class="tactic">exact</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Logic.html#True">True</a></span>.<br/>
Defined.</div>
<div class="toggleproof" onclick="toggleDisplay('proof7')">Next Obligation.</div>
<div class="proofscript" id="proof7">
&nbsp;&nbsp;<span class="tactic">reflexivity</span>.<br/>
Qed.</div>
<div class="toggleproof" onclick="toggleDisplay('proof8')">Next Obligation.</div>
<div class="proofscript" id="proof8">
&nbsp;&nbsp;<span class="id">constructor</span>.<br/>
&nbsp;&nbsp;<span class="tactic">intros</span> <span class="id">f</span>.<br/>
&nbsp;&nbsp;<span class="tactic">exact</span> (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_to_string">DATE_TIME_to_string</a></span> <span class="id">f</span>).<br/>
Defined.</div>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_from_string">DATE_TIME_from_string</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_from_string</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">DateTime.from_string</span> (<span class="id">Util.string_of_char_list</span> <span class="id">x</span>))".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_DURATION_from_string">DATE_TIME_DURATION_from_string</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_DURATION_from_string</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">DateTime.dfrom_string</span> (<span class="id">Util.string_of_char_list</span> <span class="id">x</span>))".<br/>
<br/>
<span class="kwd">Inductive</span> <span class="id"><a name="date_time_component">date_time_component</a></span><br/>
&nbsp;&nbsp;:=<br/>
&nbsp;&nbsp;| <span class="id"><a name="date_time_DAY">date_time_DAY</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="date_time_MONTH">date_time_MONTH</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="date_time_QUARTER">date_time_QUARTER</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="date_time_YEAR">date_time_YEAR</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_component_tostring">date_time_component_tostring</a></span> (<span class="id">part</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component">date_time_component</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#part">part</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_DAY">date_time_DAY</a></span> =&gt; "<span class="id">day</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_MONTH">date_time_MONTH</a></span> =&gt; "<span class="id">month</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_QUARTER">date_time_QUARTER</a></span> =&gt; "<span class="id">quarter</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_YEAR">date_time_YEAR</a></span> =&gt; "<span class="id">year</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Global</span> <span class="kwd">Instance</span> <span class="id"><a name="date_time_component_to_string">date_time_component_to_string</a></span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.CoqLibAdd.html#ToString">ToString</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component">date_time_component</a></span><br/>
&nbsp;&nbsp;:= { <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.CoqLibAdd.html#toString">toString</a></span> := <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component_tostring">date_time_component_tostring</a></span> }.<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_day">DATE_TIME_day</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_day</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">DateTime.day</span> <span class="id">x</span>)".<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_month">DATE_TIME_month</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_month</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">DateTime.month</span> <span class="id">x</span>)".<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_quarter">DATE_TIME_quarter</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_quarter</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">DateTime.quarter</span> <span class="id">x</span>)".<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_year">DATE_TIME_year</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_year</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> -&gt; <span class="id">DateTime.year</span> <span class="id">x</span>)".<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="DATE_TIME_component">DATE_TIME_component</a></span> (<span class="id">part</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component">date_time_component</a></span>) (<span class="id">dt</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Numbers.BinNums.html#Z">Z</a></span> :=<br/>
&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#part">part</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_DAY">date_time_DAY</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_day">DATE_TIME_day</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#dt">dt</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_MONTH">date_time_MONTH</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_month">DATE_TIME_month</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#dt">dt</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_QUARTER">date_time_QUARTER</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_quarter">DATE_TIME_quarter</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#dt">dt</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_YEAR">date_time_YEAR</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_year">DATE_TIME_year</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#dt">dt</a></span><br/>
&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Inductive</span> <span class="id"><a name="date_time_unary_op">date_time_unary_op</a></span><br/>
&nbsp;&nbsp;:=<br/>
&nbsp;&nbsp;| <span class="id"><a name="uop_date_time_component">uop_date_time_component</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component">date_time_component</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_unary_op">date_time_unary_op</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="uop_date_time_from_string">uop_date_time_from_string</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="uop_date_time_duration_from_string">uop_date_time_duration_from_string</a></span><br/>
.<br/>
<br/>
<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string</span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_unary_op_tostring">date_time_unary_op_tostring</a></span> (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_unary_op">date_time_unary_op</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f">f</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_component">uop_date_time_component</a></span> <span class="id">part</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"(<span class="id">dateTimeComponent</span>" ++ (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component_tostring">date_time_component_tostring</a></span> <span class="id">part</span>) ++ ")"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_from_string">uop_date_time_from_string</a></span> =&gt; "<span class="id">DateTimeFromString</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_duration_from_string">uop_date_time_duration_from_string</a></span> =&gt; "<span class="id">DateTimeDurationFromString</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.ForeignToJava.html">Qcert.Translation.ForeignToJava</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html">Qcert.Translation.NNRCtoJava</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_component_to_java_string">date_time_component_to_java_string</a></span> (<span class="id">part</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component">date_time_component</a></span>): <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#part">part</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_DAY">date_time_DAY</a></span> =&gt; "<span class="id">UnaryOperators.day</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_MONTH">date_time_MONTH</a></span> =&gt; "<span class="id">UnaryOperators.month</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_QUARTER">date_time_QUARTER</a></span> =&gt; "<span class="id">UnaryOperators.quarter</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_YEAR">date_time_YEAR</a></span> =&gt; "<span class="id">UnaryOperators.year</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_to_java_unary_op">date_time_to_java_unary_op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">indent</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>) (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>) (<span class="id">fu</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_unary_op">date_time_unary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.ForeignToJava.html#java_json">java_json</a></span>) : <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.ForeignToJava.html#java_json">java_json</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#fu">fu</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_component">uop_date_time_component</a></span> <span class="id">part</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_unary_op1">mk_java_unary_op1</a></span> "<span class="id">date_time_component</span>" (<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_component_to_java_string">date_time_component_to_java_string</a></span> <span class="id">part</span>) <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d">d</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_from_string">uop_date_time_from_string</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_unary_op0">mk_java_unary_op0</a></span> "<span class="id">date_time_from_string</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d">d</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_duration_from_string">uop_date_time_duration_from_string</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_unary_op0">mk_java_unary_op0</a></span> "<span class="id">date_time_duration_from_string</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d">d</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_to_javascript_unary_op">date_time_to_javascript_unary_op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">indent</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>) (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>) (<span class="id">fu</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_unary_op">date_time_unary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#fu">fu</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_component">uop_date_time_component</a></span> <span class="id">part</span> =&gt; "<span class="id">dateTimeComponent</span>(" ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#quotel">quotel</a></span> ++ (<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.CoqLibAdd.html#toString">toString</a></span> <span class="id">part</span>) ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#quotel">quotel</a></span> ++ ", " ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d">d</a></span> ++ ")"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_from_string">uop_date_time_from_string</a></span> =&gt; "<span class="id">dateTimeFromString</span>(" ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d">d</a></span> ++ ")"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_duration_from_string">uop_date_time_duration_from_string</a></span> =&gt; "<span class="id">dateTimeDurationFromString</span>(" ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d">d</a></span> ++ ")"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_to_ajavascript_unary_op">date_time_to_ajavascript_unary_op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fu</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_unary_op">date_time_unary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">e</span>:<span class="id">JsSyntax.expr</span>) : <span class="id">JsSyntax.expr</span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#fu">fu</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_component">uop_date_time_component</a></span> <span class="id">part</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimeComponent</span>" [ <span class="id">expr_literal</span> (<span class="id">literal_string</span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.CoqLibAdd.html#toString">toString</a></span> <span class="id">part</span>)); <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e">e</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_from_string">uop_date_time_from_string</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimeFromString</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e">e</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#uop_date_time_duration_from_string">uop_date_time_duration_from_string</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimeDurationFromString</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e">e</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_plus">DATE_TIME_plus</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_plus</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.plus</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_minus">DATE_TIME_minus</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_minus</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt;  <span class="id">DateTime.minus</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_ne">DATE_TIME_ne</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_ne</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.ne</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_lt">DATE_TIME_lt</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_lt</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.lt</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_le">DATE_TIME_le</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_le</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.le</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_gt">DATE_TIME_gt</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_gt</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.gt</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_ge">DATE_TIME_ge</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#bool">bool</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_ge</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.ge</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_DURATION_duration">DATE_TIME_DURATION_duration</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME_DURATION">DATE_TIME_DURATION</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_DURATION_duration</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.dduration</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_DURATION_days">DATE_TIME_DURATION_days</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Float.html#float">float</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_DURATION_days</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.ddays</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Axiom</span> <span class="id"><a name="DATE_TIME_DURATION_seconds">DATE_TIME_DURATION_seconds</a></span> : <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#DATE_TIME">DATE_TIME</a></span> -&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Float.html#float">float</a></span>.<br/>
<span class="id">Extract</span> <span class="id">Inlined</span> <span class="id">Constant</span> <span class="id">DATE_TIME_DURATION_seconds</span> =&gt; "(<span class="kwd">fun</span> <span class="id">x</span> <span class="id">y</span> -&gt; <span class="id">DateTime.dseconds</span> <span class="id">x</span> <span class="id">y</span>)".<br/>
<br/>
<span class="kwd">Inductive</span> <span class="id"><a name="date_time_binary_op">date_time_binary_op</a></span><br/>
&nbsp;&nbsp;:=<br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_plus">bop_date_time_plus</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_minus">bop_date_time_minus</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_ne">bop_date_time_ne</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_lt">bop_date_time_lt</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_le">bop_date_time_le</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_gt">bop_date_time_gt</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_ge">bop_date_time_ge</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_duration">bop_date_time_duration</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_duration_days">bop_date_time_duration_days</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="bop_date_time_duration_seconds">bop_date_time_duration_seconds</a></span><br/>
.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_binary_op_tostring">date_time_binary_op_tostring</a></span> (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_binary_op">date_time_binary_op</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#f">f</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_plus">bop_date_time_plus</a></span> =&gt; "<span class="id">DateTimePlus</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_minus">bop_date_time_minus</a></span> =&gt; "<span class="id">DateTimeMinus</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ne">bop_date_time_ne</a></span> =&gt; "<span class="id">DateTimeNe</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_lt">bop_date_time_lt</a></span> =&gt; "<span class="id">DateTimeLt</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_le">bop_date_time_le</a></span> =&gt; "<span class="id">DateTimeLe</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_gt">bop_date_time_gt</a></span> =&gt; "<span class="id">DateTimeGt</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ge">bop_date_time_ge</a></span> =&gt; "<span class="id">DateTimeGe</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration">bop_date_time_duration</a></span> =&gt; "<span class="id">DateTimeDiff</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_days">bop_date_time_duration_days</a></span> =&gt; "<span class="id">DateTimeDiffDays</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_seconds">bop_date_time_duration_seconds</a></span> =&gt; "<span class="id">DateTimeDiffSeconds</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="jsFunc">jsFunc</a></span> (<span class="id">name</span> <span class="id">d1</span> <span class="id">d2</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#name">name</a></span> ++ "(" ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> ++ ", " ++ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span> ++ ")".<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_to_java_binary_op">date_time_to_java_binary_op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">indent</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>) (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>) (<span class="id">fb</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_binary_op">date_time_binary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d1</span> <span class="id">d2</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.ForeignToJava.html#java_json">java_json</a></span>) : <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.ForeignToJava.html#java_json">java_json</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#fb">fb</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_plus">bop_date_time_plus</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_plus</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_minus">bop_date_time_minus</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_minus</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ne">bop_date_time_ne</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_ne</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_lt">bop_date_time_lt</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_lt</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_le">bop_date_time_le</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_le</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_gt">bop_date_time_gt</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_gt</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ge">bop_date_time_ge</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_ge</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration">bop_date_time_duration</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_duration</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_days">bop_date_time_duration_days</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_duration_days</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_seconds">bop_date_time_duration_seconds</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJava.html#mk_java_binary_op0">mk_java_binary_op0</a></span> "<span class="id">date_time_duration_seconds</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_to_javascript_binary_op">date_time_to_javascript_binary_op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">indent</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>) (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>) (<span class="id">fb</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_binary_op">date_time_binary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d1</span> <span class="id">d2</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#fb">fb</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_plus">bop_date_time_plus</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimePointPlus</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_minus">bop_date_time_minus</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimePointMinus</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ne">bop_date_time_ne</a></span> =&gt;  <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimePointNe</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_lt">bop_date_time_lt</a></span> =&gt;  <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimePointLt</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_le">bop_date_time_le</a></span> =&gt;  <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimePointLe</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_gt">bop_date_time_gt</a></span> =&gt;  <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimePointGt</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ge">bop_date_time_ge</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimePointGe</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration">bop_date_time_duration</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimeDuration</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_days">bop_date_time_duration_days</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimeDurationDays</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_seconds">bop_date_time_duration_seconds</a></span> =&gt; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#jsFunc">jsFunc</a></span> "<span class="id">dateTimeDurationSeconds</span>" <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d1">d1</a></span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#d2">d2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.  <br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="date_time_to_ajavascript_binary_op">date_time_to_ajavascript_binary_op</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fb</span>:<span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#date_time_binary_op">date_time_binary_op</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">e1</span> <span class="id">e2</span>:<span class="id">JsSyntax.expr</span>) : <span class="id">JsSyntax.expr</span><br/>
&nbsp;&nbsp;:= <span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#fb">fb</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_plus">bop_date_time_plus</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimePointPlus</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_minus">bop_date_time_minus</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimePointMinus</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ne">bop_date_time_ne</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimePointNe</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_lt">bop_date_time_lt</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimePointLt</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_le">bop_date_time_le</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimePointLe</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_gt">bop_date_time_gt</a></span> =&gt;  <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimePointGt</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_ge">bop_date_time_ge</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimePointGe</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration">bop_date_time_duration</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimeDuration</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_days">bop_date_time_duration_days</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimeDurationDays</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#bop_date_time_duration_seconds">bop_date_time_duration_seconds</a></span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.JavaScriptAst.Lang.JavaScriptAstUtil.html#call_runtime">call_runtime</a></span> "<span class="id">dateTimeDurationSeconds</span>" [ <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e1">e1</a></span>; <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html#e2">e2</a></span> ]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.  <br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
